Step of Proof: hd_member
11,40
postcript
pdf
Inference at
*
1
I
of proof for Lemma
hd
member
:
1.
T
: Type
2.
True
([]
[])
latex
by ((D (-1)
)
CollapseTHEN (Auto
))
latex
C
.
Definitions
A
,
P
Q
,
False
,
True
,
t
T
origin
True
([] 
[])
by ((D (-1)
)
CollapseTHEN (Auto))
C.True
([] [])
by ((D (-1))
CollapseTHEN (Auto))
C.A
Q T